A:Type, l:IdLnk, tg:Id, ds:x:Id fp Type, conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
(k:Knd. (k  dom(conds))  (hasloc(k;source(l))))
 Normal(ds)
 Normal(A)
 (k:Knd. (k  fpf-domain(conds))  ((conds(k).1) & ((k = rcv(l,tg)))))
 es.triggers-glued-p(es; A; l; tg; ds; conds) 

latex

Definitions

False, Type, t  T, s = t, Knd, x:AB(x), x:A. B(x), P  Q, x:A  B(x), IdLnk, Atom$n, Id, a:A fp B(a), b, if b then t else f fi , xdom(f). v=f(x)   P(x;v), Normal(ds), Normal(T), R ||- es.P(es), es.P(es), left + right, a < b, (x  l), let x,y = A in B(x;y), t.1, P  Q, P & Q, P  Q, KindDeq, Top, State(ds), x.A(x), x. t(x), f(x), {x:A| B(x)} , type List, f(a), A c B, A, #$n, ||as||, Void, A  B, , , l[i], fpf-domain(f), , rcv(l,tg), source(l), hasloc(k;i), x  dom(f), triggers-glued-p(es; A; l; tg; ds; conds), ES, x:A. B(x), sender-glues-triggers-p(es; A; l; tg; ds; conds)

Lemmas

sender-glues-implies-triggers-glued, R-realizes wf, R-implies-rule, event system wf, triggers-glued-p wf, sender-glues-triggers-p wf, sender-glues-triggers-realizable, fpf wf, fpf-dom wf, assert wf, hasloc wf, lsrc wf, normal-ds wf, normal-type wf, Kind-deq wf, rcv wf, Knd wf, l member wf, not wf, IdLnk wf, Id wf, length wf nat, fpf-domain wf, nat wf, select wf, fpf-trivial-subtype-top, pi1 wf, fpf-ap wf, decl-state wf, top wf, member-fpf-dom, false wf